/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.jmlsyp.collections;

import com.googlecode.syper.anno.BoundsChecks;
import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Imm;
import com.googlecode.syper.anno.NullChecks;
import com.googlecode.syper.anno.ReturnExcl;
import com.googlecode.syper.anno.ReturnImm;

import edu.cmu.cs.crystal.annotations.PassingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;

/**
 * {@code int} set represented as a sorted binary tree with recursive operations.
 * For specification purposes only each tree node holds an array with the 
 * {@code int}s currently in the conceptual (sub-) set represented by the node.
 * An empty set has no root node, otherwise the root node's array contains the
 * elements of the set.
 * This allows specifying the various set operations in terms of the root node.
 * @author kevin
 * @since Aug 7, 2010
 */
@NullChecks
@BoundsChecks
@PassingTest
@UseAnalyses("SymbolicChecker")
public class RecursiveIntTreeSetWithSpecArray {

	@Excl private Node root;
	
	//@ public invariant root == null || (root.contents != null & 0 < root.contents.length & root.contents[0] == root.v);
	
	/**
	 * Empties the set.
	 * This is an additional method not present in Jahob example.
	 */
	//@ ensures root == null;
	@Excl(mod = "root")
	public void clear() {
		excl: root = null;
	}
	
	//@ ensures root != null & root.contents != null & 0 < root.contents.length;
	//@ ensures (\exists int k; 0 <= k & k < root.contents.length; root.contents[k] == v);
	// set extension:
	//@ ensures \old(root) == null ? 
	//@  	(\forall int l; 0 <= l & l < root.contents.length; root.contents[l] == v) :
	//@  	\old(root.contents) != null 
	//@  	& (\forall int k; 0 <= k & k < \old(root.contents).length;
	//@  		(\exists int l; 0 <= l & l < root.contents.length; \old(root.contents[k]) == root.contents[l]));
	//@ ensures (\forall int k; 0 <= k & k < root.contents.length; root.contents[k] == v
	//@  	|| (\old(root) != null & (\exists int l; 0 <= l & l < \old(root.contents).length; root.contents[k] == \old(root.contents[l]))));
	@Excl(mod = "root")
	public void add(int v) {
		excl: {
			if (root == null)
				root = new Node(v);
			else
				root.add(v);
		}
	}
	
	//@ ensures \result == (root != null && (\exists int k; 0 <= k & k < root.contents.length; root.contents[k] == v));
	@Imm
	public boolean contains(int v) {
		imm: {
			if (root == null)
				return false;
			else
				return root.contains(v);
		}
	}
	
	//@ ensures \result == (root == null);
	@Imm
	public boolean isEmpty() {
		imm: return root == null;
	}
	
	//@ requires root != null;
	//@ ensures root == null 
	//@  	|| (\forall int k; 0 <= k & k < root.contents.length; root.contents[k] != v
	// set contraction:
	//@  		& (\exists int l; 0 <= l & l < \old(root.contents).length; root.contents[k] == \old(root.contents[l])));
	//@ ensures (\forall int k; 0 <= k & k < \old(root.contents).length; \old(root.contents[k]) == v 
	//@  	|| (root != null & root.contents != null 
	//@  		& (\exists int l; 0 <= l & l < root.contents.length; \old(root.contents[k]) == root.contents[l])));
	@Excl(mod = "root")
	public void remove(int v) {
		excl: {
			if (root.getValue() == v) {
				root = root.cut();
			} else {
				root.remove(v);
			}
		}
	}
	
	//@ requires root != null;
	//@ ensures (\exists int k; 0 <= k & k < \old(root.contents).length; \result == \old(root.contents[k]));
	//@ ensures (\forall int k; 0 <= k & k < \old(root.contents).length; \result <= \old(root.contents[k]));
	//@ ensures root == null
	//@  	|| (\forall int k; 0 <= k & k < root.contents.length; \result < root.contents[k]
	// set contraction:
	//@  		& (\exists int l; 0 <= l & l < \old(root.contents).length; root.contents[k] == \old(root.contents[l])));
	//@ ensures (\forall int k; 0 <= k & k < \old(root.contents).length; \old(root.contents[k]) == \result
	//@  	|| (root != null & root.contents != null 
	//@  		& (\exists int l; 0 <= l & l < root.contents.length; \old(root.contents[k]) == root.contents[l])));
	@Excl(mod = "root")
	public int extractMin() {
		excl: {
			if (root.hasLeft()) {
				@Excl(borrowed = false) Node min = root.extractMinChild();
				return min.getValue();
			} else {
				// root itself is minimum node in the tree
				int result = root.getValue();
				root = root.dropRight();
				return result;
			}
		}
	}
	
	//@ requires root != null;
	//@ ensures (\exists int k; 0 <= k & k < \old(root.contents).length; \result == \old(root.contents[k]));
	//@ ensures (\forall int k; 0 <= k & k < \old(root.contents).length; \old(root.contents[k]) <= \result);
	//@ ensures root == null || (\forall int k; 0 <= k & k < root.contents.length; root.contents[k] < \result
	// set contraction:
	//@  		& (\exists int l; 0 <= l & l < \old(root.contents).length; root.contents[k] == \old(root.contents[l])));
	//@ ensures (\forall int k; 0 <= k & k < \old(root.contents).length; \old(root.contents[k]) == \result
	//@  	|| (root != null & root.contents != null 
	//@  		& (\exists int l; 0 <= l & l < root.contents.length; \old(root.contents[k]) == root.contents[l])));
	@Excl(mod = "root")
	public int extractMax() {
		excl: {
			if (root.hasRight()) {
				@Excl(borrowed = false) Node min = root.extractMaxChild();
				return min.getValue();
			} else {
				// root itself is maximum node in the tree
				int result = root.getValue();
				root = root.dropLeft();
				return result;
			}
		}
	}

	/**
	 * Sorted binary tree node with specification-only {@link #contents} representing
	 * the set of all numbers held by this node and its transitive children. 
	 * @author kevin
	 */
	private static class Node {

		private final int v;
		@Excl private Node left;
		@Excl private Node right;
		@Excl private int[] contents;
		
		//@ public invariant (contents != null & 0 < contents.length & contents[0] == v);
		
		/*@ private invariant (\forall int k; 0 <= k & k < contents.length; contents[k] <= v | 
				(right != null & right.contents != null & 0 < right.contents.length 
				& (\exists int l; 0 <= l & l < right.contents.length; contents[k] == right.contents[l]) 
				));
			private invariant (\forall int k; 0 <= k & k < contents.length; v <= contents[k] | 
				(left != null & left.contents != null & 0 < left.contents.length 
				& (\exists int l; 0 <= l & l < left.contents.length; contents[k] == left.contents[l]) 
				));
			private invariant left == null || 
					(left.v < v & left.contents != null
					& 0 < left.contents.length & left.contents[0] == left.v
					& (\forall int k; 0 <= k & k < left.contents.length; left.contents[k] < v 
						& (\exists int l; 0 <= l & l < contents.length; left.contents[k] == contents[l])
					));
			private invariant right == null || 
					(v < right.v & right.contents != null
					& 0 < right.contents.length & right.contents[0] == right.v
					& (\forall int k; 0 <= k & k < right.contents.length; v < right.contents[k] 
						& (\exists int l; 0 <= l & l < contents.length; right.contents[k] == contents[l])
					));
		*/

		//@ ensures this.v == v & this.left == null & this.right == null;
		//@ ensures this.contents != null & this.contents.length == 1 & this.contents[0] == v;
		public Node(int v) {
			this.v = v;
			this.left = null;
			this.right = null;
			this.contents = new int[] { v };
		}
		
		/* accessors */

		/**
		 * Returns {@link #v}
		 * @return {@link #v}
		 */
		//@ ensures \result == v;
		@Imm public int getValue() { 
			imm: return v; 
		}
		
		/**
		 * Returns whether there is a left subtree, 
		 * which means there are numbers strictly smaller than {@link #v} in the set
		 * @return {@code false} if {@link #left} is {@code null}, {@code true} otherwise
		 */
		//@ ensures \result == (left != null);
		//@ ensures \result == (\exists int k; 0 <= k & k < contents.length; contents[k] < v);
		@Imm public boolean hasLeft() {
			imm: return left != null;
		}
		
		/**
		 * Returns whether there is a right subtree, 
		 * which means there are numbers strictly larger than {@link #v} in the set
		 * @return {@code false} if {@link #right} is {@code null}, {@code true} otherwise
		 */
		//@ ensures \result == (right != null);
		//@ ensures \result == (\exists int k; 0 <= k & k < contents.length; v < contents[k]);
		@Imm public boolean hasRight() {
			imm: return right != null;
		}
		
		/**
		 * this method gives read-only access to childrens' {@link #contents}
		 * for {@link #putLeft(Node)} and {@link #putRight(Node)}
		 * @return read-only reference to {@link #contents}
		 */
		//@ ensures \result != null & \result == contents;
		@ReturnImm @Imm(released = true) 
		private int[] getContents() {
			imm: return contents;
		}
		
		//@ ensures contents != null & contents.length == \old(contents.length) + 1;
		//@ ensures contents[contents.length - 1] == w;
		//@ ensures (\forall int k; 0 <= k & k < \old(contents.length); \old(contents[k]) == contents[k]);
		@Excl(mod = {"left", "right", "contents"})
		public boolean add(final int w) {
			excl: {
				boolean added = true;
				if (w < v) {
					if (left == null) {
						left = new Node(w);
					} else {
						added = left.add(w);
					}
				} else if (v < w) {
					if (right == null) {
						right = new Node(w);
					} else {
						added = right.add(w);
					}
				} else {
					added = false;
				}
				
				contents = copyOf(contents, 1);
				contents[contents.length - 1] = w;
				return added;
			}
		}

		//@ ensures \result == (\exists int k; 0 <= k & k < contents.length; contents[k] == w);
		@Imm public boolean contains(final int w) {
			imm: {
				final boolean result;
				if (w == v)
					result = true;
				else if (w < v)
					result = left == null ? false : left.contains(w);
				else 
					result = right == null ? false : right.contains(w);
				return result;
			}
		}

		//@ requires w != v;
		//@ ensures (\forall int k; 0 <= k & k < contents.length; 
		//@  	\old(contents[k]) == w ? contents[k] == v : contents[k] == \old(contents[k]));
		@Excl(mod = {"left", "right"})
		public boolean remove(int w) {
			excl: {
				if (w < v) {
					if (left == null) {
						return false;
					} else if (left.getValue() == w) {
						left = left.cut();
						final Node oldL = left;
						int i = 0;
						//@ maintaining 0 <= i & i <= contents.length;
						//@ maintaining left == oldL & right == \old(right);
						//@ maintaining (\forall int k; 0 <= k & k < i; 
						//@  	\old(contents[k]) == w ? contents[k] == v : contents[k] == \old(contents[k]));
						//@ maintaining (\forall int k; i <= k & k < contents.length; 
						//@  	\old(contents[k]) == w ? contents[k] == w : contents[k] == \old(contents[k]));
						//@ maintaining (\forall int k; 0 <= k & k < i; v <= contents[k] | 
						//@  	(left != null & left.contents != null & 0 < left.contents.length 
						//@  	& (\exists int l2; 0 <= l2 & l2 < left.contents.length; contents[k] == left.contents[l2]) 
						//@ ));
						//@ maintaining (\forall int k; i <= k & k < contents.length; v <= contents[k] | w == contents[k] | 
						//@  	(left != null & left.contents != null & 0 < left.contents.length 
						//@  	& (\exists int l2; 0 <= l2 & l2 < left.contents.length; contents[k] == left.contents[l2]) 
						//@ ));
						for (; i < contents.length; ++i) {
							if (contents[i] == w)
								contents[i] = v;
						}
					} else {
						left.remove(w);
						final Node oldL = left;
						int i = 0;
						//@ maintaining 0 <= i & i <= contents.length;
						//@ maintaining left == oldL & right == \old(right);
						//@ maintaining (\forall int k; 0 <= k & k < i; 
						//@  	\old(contents[k]) == w ? contents[k] == v : contents[k] == \old(contents[k]));
						//@ maintaining (\forall int k; i <= k & k < contents.length; 
						//@  	\old(contents[k]) == w ? contents[k] == w : contents[k] == \old(contents[k]));
						for (; i < contents.length; ++i) {
							if (contents[i] == w)
								contents[i] = v;
						}
					}
				} else {
					assert v < w;
					if (right == null) {
						return false;
					} else if (right.getValue() == w) {
						right = right.cut();
						final Node oldR = right;
						int i = 0;
						//@ maintaining 0 <= i & i <= contents.length;
						//@ maintaining right == oldR & left == \old(left);
						//@ maintaining (\forall int k; 0 <= k & k < i; 
						//@  	\old(contents[k]) == w ? contents[k] == v : contents[k] == \old(contents[k]));
						//@ maintaining (\forall int k; i <= k & k < contents.length; 
						//@  	\old(contents[k]) == w ? contents[k] == w : contents[k] == \old(contents[k]));
						//@ maintaining (\forall int k; 0 <= k & k < i; contents[k] <= v | 
						//@  	(right != null & right.contents != null & 0 < right.contents.length 
						//@  	& (\exists int l2; 0 <= l2 & l2 < right.contents.length; contents[k] == right.contents[l2]) 
						//@ ));
						//@ maintaining (\forall int k; i <= k & k < contents.length; contents[k] <= v | w == contents[k] | 
						//@  	(right != null & right.contents != null & 0 < right.contents.length 
						//@  	& (\exists int l2; 0 <= l2 & l2 < right.contents.length; contents[k] == right.contents[l2]) 
						//@ ));
						for (; i < contents.length; ++i) {
							if (contents[i] == w)
								contents[i] = v;
						}
					} else {
						right.remove(w);
						final Node oldR = right;
						int i = 0;
						//@ maintaining 0 <= i & i <= contents.length;
						//@ maintaining right == oldR & left == \old(left);
						//@ maintaining (\forall int k; 0 <= k & k < i; 
						//@  	\old(contents[k]) == w ? contents[k] == v : contents[k] == \old(contents[k]));
						//@ maintaining (\forall int k; i <= k & k < contents.length; 
						//@  	\old(contents[k]) == w ? contents[k] == w : contents[k] == \old(contents[k]));
						for (; i < contents.length; ++i) {
							if (contents[i] == w)
								contents[i] = v;
						}
					}
				}
			}
			return true;
		}

		/**
		 * Cuts the receiver node out of the tree and returns
		 * its own replacement
		 * @return Node to replace the receiver in the tree
		 */
		//@ ensures \result == null
		//@ || (\result.contents != null
		//@  	& 0 < \result.contents.length & \result.contents[0] == \result.v
		//@  	& (\forall int k; 0 <= k & k < \result.contents.length; \result.contents[k] != v
		//@  		& (\exists int l; 0 <= l & l < \old(contents).length; \result.contents[k] == \old(contents[l]))));
		//@ ensures (\forall int k; 0 <= k & k < \old(contents).length; \old(contents[k]) == v |
		//@  	(\result != null & \result.contents != null
		//@  	& (\exists int l; 0 <= l & l < \result.contents.length; \result.contents[l] == \old(contents[k]))));
		@Excl(mod = {"left", "right", "contents"})
		@ReturnExcl public Node cut() {
			excl: {
				@Excl(borrowed = false) final Node result;
				if (left == null) {
					if (right == null) {
						result = null;
					} else {
						result = right;
						right = null;
					}
				} else {
					if (right == null) {
						result = left;
						left = null;
					} else {
						if (right.hasLeft()) {
							// find the minimum node following this one
							result = right.extractMinChild();
							result.putRight(right);
						} else {
							// right itself is min node in right subtree
							result = right;
						}
						// assume result.left == null;
						result.putLeft(left);
						right = null;
						left = null;
					}
				}
				// no children left, jam in default contents
				contents = new int[] { v };
				return result;
			}
		}

		/**
		 * Helper method for {@link #cut()} that replaces the left subtree with the given node.
		 * @param lt new left subtree, may be {@code null}
		 * @return previous left subtree, may be {@code null}
		 */
		// these are so the method can be implemented
		//@ requires lt == null || (lt.v < v & lt.contents != null
		//@  	& 0 < lt.contents.length & lt.contents[0] == lt.v
		//@  	& (\forall int i; 0 <= i & i < lt.contents.length; lt.contents[i] < v));
		//@ ensures left == lt;
		// the rest is for cut():
		//@ ensures contents != null & 0 < contents.length & \old(contents).length <= contents.length & contents[0] == v;
		//@ ensures \old(left) != null |(\forall int k; 0 <= k & k < \old(contents).length; contents[k] == \old(contents[k]));
		//@ ensures lt == null
		//@ || (\forall int k; 0 <= k & k < \old(lt.contents).length;
		//@  	(\exists int l; 0 <= l & l < contents.length; \old(lt.contents[k]) == contents[l]));
		//@ ensures \old(left) != null | (\forall int k; 0 <= k & k < contents.length; v <= contents[k]
		//@  	? k < \old(contents).length & contents[k] == \old(contents[k])
		//@  	: lt != null & (\exists int l; 0 <= l & l < \old(lt.contents).length; contents[k] == \old(lt.contents[l]))); 
		@Excl(mod = {"left", "contents"}) @ReturnExcl 
		private Node putLeft(@Excl(borrowed = false) final Node lt) {
			@Excl(borrowed = false) final Node result = dropLeft();

			if (lt != null) excl: {
				{ // need extra block to keep leftC in local variable
					@Imm final int[] oldC = contents;
					@Imm final int[] leftC = lt.getContents();
					@Excl(borrowed = false) final int[] newC = copyOf(contents, leftC.length);
					
					int i = 0;
					//@ maintaining 0 <= i & i <= leftC.length & oldC == contents & oldC.length == contents.length;
					//@ maintaining newC[0] == v;
					//@ maintaining \old(left) != null 
					//@  	| (\forall int k; 0 <= k & k < \old(contents).length; newC[k] == \old(contents[k]));
					//@ maintaining (\forall int k; 0 <= k & k < contents.length; newC[k] == v |
					//@     (v < newC[k] & right != null & right.contents != null & 0 < right.contents.length
					//@ 	& (\exists int l; 0 <= l & l < right.contents.length; newC[k] == right.contents[l])));
					//@ maintaining right == null || 
					//@     (v < right.v & right.contents != null &
					//@     (\forall int k; 0 <= k & k < right.contents.length; v < right.contents[k] 
					//@     & (\exists int l; 0 <= l & l < contents.length; right.contents[k] == newC[l]))); 
					//@ maintaining (\forall int k; contents.length <= k & k < contents.length + i; 
					//@     newC[k] == leftC[k - contents.length] & newC[k] < v);
					for (; i < leftC.length; ++i) {
						newC[contents.length + i] = leftC[i];
					}
					// this is a lemma! a hint to the prover that it can't figure out itself
					// this can alternatively be made an additional loop invariant
					//@ assert (\forall int k; 0 <= k & k < leftC.length; leftC[k] == newC[k + contents.length] & leftC[k] < v);
					contents = newC;
				}
				left = lt;
			}
			return result; 
		}

		/**
		 * Helper method for {@link #putLeft(Node)} that drops
		 * any existing left node, including fixing {@link #contents}.
		 * @return the dropped left node
		 */
		//@ ensures left == null & \result == \old(left);
		//@ ensures contents != null & 0 < contents.length & contents.length == \old(contents).length & contents[0] == v; 
		//@ ensures (\forall int k; 0 <= k & k < contents.length; \old(contents[k]) < v | \old(contents[k]) == contents[k]);
		//@ ensures (\forall int k; 0 <= k & k < contents.length; v <= \old(contents[k]) | 
		//@ 			(\result != null & \result.contents != null
		//@ 			& (\exists int l; 0 <= l & l < \result.contents.length; \result.contents[l] == \old(contents[k]))));
		//@ ensures \result == null ||
		//@ 	(\result.v < v & \result.contents != null & 0 < \result.contents.length & \result.contents[0] == \result.v
		//@  	& (\exists int k; 0 <= k & k < \old(contents).length; \result.v == \old(contents[k]))
		//@ 	& (\forall int k; 0 <= k & k < \result.contents.length; \result.contents[k] < v
		//@ 		& (\exists int l; 0 <= l & l < \old(contents).length; \result.contents[k] == \old(contents[l]))));
		@Excl(mod = "left") @ReturnExcl
		private Node dropLeft() { excl: {
			@Excl(borrowed = false) final Node result = left;
			
			int i = 0;
			//@ maintaining contents != null & 0 < contents.length & contents[0] == v; 
			//@ maintaining 0 <= i & i <= contents.length;
			//@ maintaining (\forall int k; 0 <= k & k < contents.length; contents[k] <= v |
			//@     (right != null & right.contents != null & 0 < right.contents.length
			//@     & (\exists int l; 0 <= l & l < right.contents.length; contents[k] == right.contents[l])));
			//@ maintaining right == null || 
			//@     (v < right.v & right.contents != null
			//@ 	& (\forall int k; 0 <= k & k < right.contents.length; v < right.contents[k] 
			//@ 		& (\exists int l; 0 <= l & l < contents.length; right.contents[k] == contents[l])));
			//@ maintaining (\forall int k; 0 <= k & k < i; v <= contents[k] & (\old(contents[k]) < v | \old(contents[k]) == contents[k]));
			//@ maintaining (\forall int k; i <= k & k < contents.length; contents[k] == \old(contents[k]));
			for (; i < contents.length; ++i) {
				if (contents[i] < v)
					contents[i] = v;
			}
			left = null;
			return result;
		} }		

		/**
		 * Helper method for {@link #cut()} that replaces the right subtree with the given node
		 * @param rt new right subtree, may be {@code null}
		 * @return previous right subtree, may be {@code null}
		 */
		// these are so the method can be implemented
		//@ requires rt == null || (v < rt.v & rt.contents != null
		//@  	& 0 < rt.contents.length & rt.contents[0] == rt.v
		//@  	& (\forall int i; 0 <= i & i < rt.contents.length; v < rt.contents[i]));
		//@ ensures right == rt;
		// the rest is for cut():
		//@ ensures contents != null & 0 < contents.length & \old(contents).length <= contents.length & contents[0] == v;
		//@ ensures \old(right) != null | (\forall int k; 0 <= k & k < \old(contents).length; contents[k] == \old(contents[k]));
		//@ ensures rt == null
		//@ || (\forall int k; 0 <= k & k < \old(rt.contents).length;
		//@  	(\exists int l; 0 <= l & l < contents.length; \old(rt.contents[k]) == contents[l]));
		//@ ensures \old(right) != null | (\forall int k; 0 <= k & k < contents.length; contents[k] <= v
		//@  	? k < \old(contents).length & contents[k] == \old(contents[k])
		//@  	: rt != null & (\exists int l; 0 <= l & l < \old(rt.contents).length; contents[k] == \old(rt.contents[l]))); 
		@Excl(mod = {"right", "contents"}) @ReturnExcl 
		private Node putRight(@Excl(borrowed = false) final Node rt) {
			@Excl(borrowed = false) final Node result = dropRight();

			if (rt != null) excl: { 
				{ // need extra block to keep rightC in local variable
					@Imm final int[] oldC = contents;
					@Imm final int[] rightC = rt.getContents();
					@Excl(borrowed = false) final int[] newC = copyOf(contents, rightC.length);
					
					int i = 0;
					//@ maintaining 0 <= i & i <= rightC.length;
					//@ maintaining oldC == contents & oldC.length == contents.length;
					//@ maintaining newC[0] == v;
					//@ maintaining \old(right) != null 
					//@  	| (\forall int k; 0 <= k & k < \old(contents).length; newC[k] == \old(contents[k]));
					//@ maintaining (\forall int k; 0 <= k & k < contents.length; newC[k] == v |
					//@  	(newC[k] < v & left != null & left.contents != null & 0 < left.contents.length
					//@  	& (\exists int l; 0 <= l & l < left.contents.length; newC[k] == left.contents[l])));
					//@ maintaining left == null || 
					//@  	(left.v < v & left.contents != null
					//@  	& (\forall int k; 0 <= k & k < left.contents.length; left.contents[k] < v 
					//@  		& (\exists int l; 0 <= l & l < contents.length; left.contents[k] == newC[l])));
					//@ maintaining (\forall int k; contents.length <= k & k < contents.length + i; 
					//@  	newC[k] == rightC[k - contents.length] & v < newC[k]);
					for (; i < rightC.length; ++i) {
						newC[contents.length + i] = rightC[i];
					}
					// this is a lemma! a hint to the prover that it can't figure out itself
					// this can alternatively be made an additional loop invariant
					//@ assert (\forall int k; 0 <= k & k < rightC.length; rightC[k] == newC[k + contents.length] & v < rightC[k]);
					contents = newC;
				}
				right = rt;
			}
			return result; 
		}
	
		/**
		 * Helper method for {@link #putRight(Node)} that drops
		 * any existing right node, including fixing {@link #contents}.
		 * @return the dropped right node
		 */
		//@ ensures right == null & \result == \old(right);
		//@ ensures contents != null & 0 < contents.length & contents.length == \old(contents).length & contents[0] == v; 
		//@ ensures (\forall int k; 0 <= k & k < contents.length; v < \old(contents[k]) ? contents[k] == v : \old(contents[k]) == contents[k]);
		//@ ensures (\forall int k; 0 <= k & k < contents.length; \old(contents[k]) <= v | 
		//@ 			(\result != null & \result.contents != null
		//@ 			& (\exists int l; 0 <= l & l < \result.contents.length; \result.contents[l] == \old(contents[k]))));
		//@ ensures \result == null ||
		//@ 	(v < \result.v & \result.contents != null & 0 < \result.contents.length & \result.contents[0] == \result.v
		//@  	& (\exists int k; 0 <= k & k < \old(contents).length; \result.v == \old(contents[k]))
		//@ 	& (\forall int k; 0 <= k & k < \result.contents.length; v < \result.contents[k]
		//@ 		& (\exists int l; 0 <= l & l < \old(contents).length; \result.contents[k] == \old(contents[l]))));
		@Excl(mod = "right") @ReturnExcl
		private Node dropRight() { excl: {
			@Excl(borrowed = false) final Node result = right;
			
			int i = 0;
			//@ maintaining contents != null & 0 < contents.length & contents[0] == v;
			//@ maintaining 0 <= i & i <= contents.length;
			//@ maintaining (\forall int k; 0 <= k & k < contents.length; v <= contents[k] |
			//@  	(left != null & left.contents != null & 0 < left.contents.length 
			//@  	& (\exists int l; 0 <= l & l < left.contents.length; contents[k] == left.contents[l])));
			//@ maintaining left == null ||
			//@  	(left.v < v & left.contents != null
			//@  	& (\forall int k; 0 <= k & k < left.contents.length; left.contents[k] < v 
			//@  		& (\exists int l; 0 <= l & l < contents.length; left.contents[k] == contents[l])));
			//@ maintaining (\forall int k; 0 <= k & k < i; contents[k] <= v & (v < \old(contents[k]) ? contents[k] == v : \old(contents[k]) == contents[k]));
			//@ maintaining (\forall int k; i <= k & k < contents.length; contents[k] == \old(contents[k]));
			for (; i < contents.length; ++i) {
				if (v < contents[i])
					contents[i] = v;
			}
			right = null;
			return result;
		} }
		
		/**
		 * Copies the given array into a larger array with {@code extra} additional cells.
		 * @param a
		 * @param extra a positive number of additional cells
		 * @return a new array with {@code a}'s contents plus {@code extra} additional cells.
		 * @see java.util.Arrays#copyOf(int[], int)
		 */
		//@ requires a != null & 0 <= extra;
		//@ ensures \result != null & \result != a & \result.length == a.length + extra;
		//@ ensures (\forall int k; 0 <= k & k < a.length; \result[k] == a[k]);
		@ReturnExcl
		private static int[] copyOf(@Imm final int[] a, int extra) {
			@Excl(borrowed = false) final int[] result = new int[a.length + extra];
			int i = 0;
			//@ maintaining 0 <= i & i <= a.length;
			//@ maintaining (\forall int k; 0 <= k & k < i; result[k] == a[k]);
			for (; i < a.length; ++i)
				result[i] = a[i];
			return result;
		}

		/**
		 * Cuts out the child with maximum value from this node's right subtree while keeping nodes that
		 * were previously children of the returned node in the right subtree.
		 * @return Maximum child with no children of its own, never {@code null}
		 */
		//@ requires right != null;
		// to make extractMaxChild work
		//@ ensures \result != null & v < \result.v & \old(contents).length == contents.length;
		//@ ensures 0 < contents.length & contents[0] == v;
		//@ ensures (\forall int k; 0 <= k & k < contents.length; 
		//@  	\result.v <= \old(contents[k]) ? contents[k] == v : \old(contents[k]) == contents[k]);
		// here's the interesting stuff
		//@ ensures (\exists int k; 0 <= k & k < \old(contents).length; \old(contents[k]) == \result.v);
		//@ ensures (\forall int k; 0 <= k & k < \old(contents).length; \old(contents[k]) <= \result.v);
		@Excl(mod = "right") @ReturnExcl
		public Node extractMaxChild() { excl: {
			@Excl(borrowed = false) final Node result;
			// use read-only hasRight so we don't lose knowledge about right.contents
			if (right.hasRight()) {
				result = right.extractMaxChild();

				int i = 0;
				//@ maintaining 0 <= i & i <= contents.length;
				// needed because right is assignable, hence havoc'ed around the loop:
				//@ maintaining right == \old(right);
				//@ maintaining (\forall int k; 0 <= k & k < i; 
				//@  	result.v <= \old(contents[k]) ? contents[k] == v : \old(contents[k]) == contents[k]);
				//@ maintaining (\forall int k; i <= k & k < contents.length; \old(contents[k]) == contents[k]);
				for (; i < contents.length; ++i) {
					if (result.getValue() <= contents[i])
						contents[i] = v;
				}
				return result;
			} else {
				// right is maximum child
				// assert (\forall int k; 0 <= k & k < contents.length; contents[k] <= right.v);
				result = right;
				right = result.dropLeft();
				
				int i = 0;
				//@ maintaining contents != null & 0 < contents.length & contents[0] == v;
				//@ maintaining 0 <= i & i <= contents.length;
				//@ maintaining \old(contents) != null & \old(contents).length == contents.length;
				//@ maintaining (\forall int k; 0 <= k & k < contents.length; v <= contents[k] |
				//@ 	(left != null & left.contents != null & 0 < left.contents.length 
				//@ 	& (\exists int l; 0 <= l & l < left.contents.length; contents[k] == left.contents[l])));
				//@ maintaining (\forall int k; 0 <= k & k < i; contents[k] <= v |
				//@ 	(right != null & right.contents != null & 0 < right.contents.length 
				//@ 	& (\exists int l; 0 <= l & l < right.contents.length; contents[k] == right.contents[l])));
				//@ maintaining (\forall int k; i <= k & k < contents.length; contents[k] <= v | result.v <= contents[k] |
				//@ 	(right != null & right.contents != null & 0 < right.contents.length 
				//@ 	& (\exists int l; 0 <= l & l < right.contents.length; contents[k] == right.contents[l])));
				//@ maintaining left == null ||
				//@ 	(left.v < v & left.contents != null &
				//@ 	(\forall int k; 0 <= k & k < left.contents.length; left.contents[k] < v 
				//@ 		& (\exists int l; 0 <= l & l < contents.length; left.contents[k] == contents[l])));
				//@ maintaining right == null || 
				//@ 	(v < right.v & right.contents != null & 0 < right.contents.length & right.contents[0] == right.v
				//@ 	& (\forall int k; 0 <= k & k < right.contents.length; v < right.contents[k] & right.contents[k] < result.v
				//@  		& (\exists int l; 0 <= l & l < contents.length; right.contents[k] == contents[l])
				//@ 	));
				//@ maintaining (\forall int k; 0 <= k & k < i; result.v <= \old(contents[k]) ? contents[k] == v : \old(contents[k]) == contents[k]);
				//@ maintaining (\forall int k; i <= k & k < contents.length; \old(contents[k]) == contents[k]);
				for (; i < contents.length; ++i) {
					if (result.getValue() <= contents[i])
						contents[i] = v;
				}
				return result;
			}
		} }

		/**
		 * Cuts out the child with minimum value from this node's left subtree while keeping nodes that
		 * were previously children of the returned node in the left subtree.
		 * @return Minimum child with no children of its own, never {@code null}
		 */
		//@ requires left != null;
		//@ ensures \result != null & \result.v < v & \result.left == null & \result.right == null;
		//@ ensures \result.contents != null & 0 < \result.contents.length & \result.contents[0] == \result.v;
		//@ ensures (\forall int k; 0 <= k & k < \result.contents.length; \result.contents[k] == \result.v);
		//@ ensures 0 < contents.length & contents[0] == v & \old(contents).length == contents.length;
		//@ ensures (\forall int k; 0 <= k & k < contents.length; 
		//@  	\old(contents[k]) <= \result.v ? contents[k] == v : \old(contents[k]) == contents[k]);
		//@ ensures (\exists int k; 0 <= k & k < \old(contents).length; \result.v == \old(contents[k]));
		//@ ensures (\forall int k; 0 <= k & k < \old(contents).length; \result.v <= \old(contents[k]));
		@Excl(mod = "left") @ReturnExcl
		public Node extractMinChild() { excl: {
			@Excl(borrowed = false) final Node result;
			// use read-only hasLeft so we don't lose knowledge about left.contents
			if (left.hasLeft()) {
				result = left.extractMinChild();

				int i = 0;
				//@ maintaining 0 <= i & i <= contents.length;
				// needed because right is assignable, hence havoc'ed around the loop:
				//@ maintaining left == \old(left);
				//@ maintaining (\forall int k; 0 <= k & k < i; 
				//@  	\old(contents[k]) <= result.v ? contents[k] == v : \old(contents[k]) == contents[k]);
				//@ maintaining (\forall int k; i <= k & k < contents.length; \old(contents[k]) == contents[k]);
				for (; i < contents.length; ++i) {
					if (contents[i] <= result.getValue())
						contents[i] = v;
				}
				return result;
			} else {
				// left is minimum child
				// assert (\forall int k; 0 <= k & k < contents.length; left.v <= contents[k]);
				result = left;
				left = result.dropRight();

				int i = 0;
				//@ maintaining contents != null & 0 < contents.length & contents[0] == v;
				//@ maintaining 0 <= i & i <= contents.length;
				//@ maintaining \old(contents) != null & \old(contents).length == contents.length;
				//@ maintaining (\forall int k; 0 <= k & k < contents.length; contents[k] <= v |
				//@ 	(right != null & right.contents != null & 0 < right.contents.length 
				//@ 	& (\exists int l; 0 <= l & l < right.contents.length; contents[k] == right.contents[l])));
				//@ maintaining (\forall int k; 0 <= k & k < i; v <= contents[k] |
				//@ 	(left != null & left.contents != null & 0 < left.contents.length 
				//@ 	& (\exists int l; 0 <= l & l < left.contents.length; contents[k] == left.contents[l])));
				//@ maintaining (\forall int k; i <= k & k < contents.length; v <= contents[k] | contents[k] <= result.v |
				//@ 	(left != null & left.contents != null & 0 < left.contents.length 
				//@ 	& (\exists int l; 0 <= l & l < left.contents.length; contents[k] == left.contents[l])));
				//@ maintaining left == null ||
				//@ 	(left.v < v & left.contents != null & 0 < left.contents.length & left.contents[0] == left.v
				//@ 	& (\forall int k; 0 <= k & k < left.contents.length; left.contents[k] < v & result.v < left.contents[k]
				//@ 		& (\exists int l; 0 <= l & l < contents.length; left.contents[k] == contents[l])));
				//@ maintaining right == null || 
				//@ 	(v < right.v & right.contents != null & 0 < right.contents.length & right.contents[0] == right.v
				//@ 	& (\forall int k; 0 <= k & k < right.contents.length; v < right.contents[k]
				//@  		& (\exists int l; 0 <= l & l < contents.length; right.contents[k] == contents[l])
				//@ 	));
				//@ maintaining (\forall int k; 0 <= k & k < i; \old(contents[k]) <= result.v ? contents[k] == v : \old(contents[k]) == contents[k]);
				//@ maintaining (\forall int k; i <= k & k < contents.length; \old(contents[k]) == contents[k]);
				for (; i < contents.length; ++i) {
					if (contents[i] <= result.getValue())
						contents[i] = v;
				}
				return result;
			}
		} }
	}
}
